\subsection{Definition}
Suppose \( F \dashv G \) is an adjunction with \( F : \mathcal C \to \mathcal D \) and \( G : \mathcal D \to \mathcal C \), where \( \mathcal C \) is a well-understood category, but \( \mathcal D \) is not.
We can study \( \mathcal D \) indirectly inside the context of \( \mathcal C \) by using the adjunction.
We have the composite \( T = GF : \mathcal C \to \mathcal C \), and we have the unit \( \eta : 1_{\mathcal C} \to T \).
The counit is not directly accessible from \( \mathcal C \), but we have \( \mu = G\epsilon_F : T^2 \to T \).
The triangular identities give rise to identities linking \( \eta \) and \( \mu \).
\[\begin{tikzcd}
	T & {T^2} \\
	& T
	\arrow["T\eta", from=1-1, to=1-2]
	\arrow["\mu", from=1-2, to=2-2]
	\arrow["{1_T}"', from=1-1, to=2-2]
\end{tikzcd}\quad\quad\begin{tikzcd}
	T & {T^2} \\
	& T
	\arrow["{\eta_T}", from=1-1, to=1-2]
	\arrow["\mu", from=1-2, to=2-2]
	\arrow["{1_T}"', from=1-1, to=2-2]
\end{tikzcd}\]
In addition, naturality of \( \epsilon \) gives
\[\begin{tikzcd}
	{T^3} & {T^2} \\
	{T^2} & T
	\arrow["T\mu", from=1-1, to=1-2]
	\arrow["\mu", from=1-2, to=2-2]
	\arrow["{\mu_T}"', from=1-1, to=2-1]
	\arrow["\mu"', from=2-1, to=2-2]
\end{tikzcd}\]
\begin{definition}
    A \emph{monad} on a category \( \mathcal C \) is a triple \( \mathbb T = (T, \eta, \mu) \) where \( T \) is a functor \( \mathcal C \to \mathcal C \), and \( \eta : 1_{\mathcal C} \to T \) and \( \mu : T^2 \to T \) are natural transformations satisfying the following commutative diagrams.
    \[\begin{tikzcd}
        T & {T^2} \\
        & T
        \arrow["T\eta", from=1-1, to=1-2]
        \arrow["\mu", from=1-2, to=2-2]
        \arrow["{1_T}"', from=1-1, to=2-2]
    \end{tikzcd}\quad\quad\begin{tikzcd}
        T & {T^2} \\
        & T
        \arrow["{\eta_T}", from=1-1, to=1-2]
        \arrow["\mu", from=1-2, to=2-2]
        \arrow["{1_T}"', from=1-1, to=2-2]
    \end{tikzcd}\quad\quad\begin{tikzcd}
        {T^3} & {T^2} \\
        {T^2} & T
        \arrow["T\mu", from=1-1, to=1-2]
        \arrow["\mu", from=1-2, to=2-2]
        \arrow["{\mu_T}"', from=1-1, to=2-1]
        \arrow["\mu"', from=2-1, to=2-2]
    \end{tikzcd}\]
    \( \eta \) is the \emph{unit} of the monad, and \( \mu \) is the \emph{multiplication} of the monad.
\end{definition}
The dual notion is called a \emph{comonad}.
\begin{example}
    \begin{enumerate}
        \item Let \( M \) be a monoid.
        The functor \( M \times (-) : \mathbf{Set} \to \mathbf{Set} \) has a monad structure.
        The unit \( \eta_A : A \to M \times A \) maps each \( a \) to \( (1, a) \), and the multiplication \( \mu_A : M \times M \times A \to M \times A \) maps \( (m, m', a) \) to \( (mm', a) \).
        These maps are natural.
        The required commutative diagrams encode precisely the left and right unit laws and the associativity law of a monoid.
        In fact, monoids correspond precisely to monads on \( \mathbf{Set} \) whose underlying functors have right adjoints.
        \item Let \( P : \mathbf{Set} \to \mathbf{Set} \) be the covariant power-set functor.
        This can be given a monad structure.
        The unit \( \eta_A : A \to PA \) maps \( a \) to its singleton \( \qty{a} \), and the multiplication \( \mu_A : PPA \to PA \) is the union operation mapping \( S \) to \( \bigcup S \).
        One can check that the required laws are satisfied.
    \end{enumerate}
\end{example}
These examples both arise as a result of adjunctions.
Example (a) arises from the free \( M \)-set functor \( F : \mathbf{Set} \to [M, \mathbf{Set}] \) and the forgetful functor \( U : [M, \mathbf{Set}] \to \mathbf{Set} \), where \( F \dashv U \).
For example (b), there is a forgetful functor \( U : \mathbf{CSLat} \to \mathbf{Set} \) from the category of complete (join-)semilattices.
This has a left adjoint \( P : \mathbf{Set} \to \mathbf{CSLat} \), which is the free complete semilattice on \( A \).
Indeed, given any \( f : A \to UB \), there is a unique extension of \( f \) to a join-preserving map \( \overline f : PA \to B \) given by
\[ \overline f(A') = \bigvee \qty{f(a') \mid a' \in A'} \]
Note that an \( M \)-set is a set \( A \) equipped with a map \( \alpha : M \times A \to A \), and a complete semilattice is a set \( A \) equipped with a map \( \bigvee : PA \to A \).
So the elements of the other category can be defined in terms of the monad.

This holds in general: every monad arises from an adjunction.
We present two constructions.

\subsection{Eilenberg--Moore algebras}
\begin{definition}
    Let \( \mathbb T = (T, \eta, \mu) \) be a monad on \( \mathcal C \).
    An \emph{Eilenberg--Moore algebra} or \emph{\( \mathbb T \)-algebra} is a pair \( (A, \alpha) \) where \( A \) is an object in \( \mathcal C \), and \( \alpha : TA \to A \) is a morphism satisfying
    % https://q.uiver.app/#q=WzAsMyxbMCwwLCJBIl0sWzEsMCwiVEEiXSxbMSwxLCJBIl0sWzAsMSwiXFxldGFfQSJdLFsxLDIsIlxcYWxwaGEiXSxbMCwyLCIxX0EiLDJdXQ==
\[\begin{tikzcd}
	A & TA \\
	& A
	\arrow["{\eta_A}", from=1-1, to=1-2]
	\arrow["\alpha", from=1-2, to=2-2]
	\arrow["{1_A}"', from=1-1, to=2-2]
\end{tikzcd}\quad\quad\begin{tikzcd}
	T^2A & TA \\
	TA & A
	\arrow["T\alpha", from=1-1, to=1-2]
	\arrow["\alpha", from=1-2, to=2-2]
	\arrow["\mu_A"', from=1-1, to=2-1]
	\arrow["\alpha"', from=2-1, to=2-2]
\end{tikzcd}\]
    A homomorphism of algebras \( f : (A, \alpha) \to (B, \beta) \) is a morphism \( f : A \to B \) such that the following diagram commutes.
    % https://q.uiver.app/#q=WzAsNCxbMCwwLCJUQSJdLFsxLDAsIlRCIl0sWzEsMSwiQiJdLFswLDEsIkEiXSxbMCwxLCJUZiJdLFsxLDIsIlxcYmV0YSJdLFswLDMsIlxcYWxwaGEiLDJdLFszLDIsImYiLDJdXQ==
\[\begin{tikzcd}
	TA & TB \\
	A & B
	\arrow["Tf", from=1-1, to=1-2]
	\arrow["\beta", from=1-2, to=2-2]
	\arrow["\alpha"', from=1-1, to=2-1]
	\arrow["f"', from=2-1, to=2-2]
\end{tikzcd}\]
    This forms a category of \( \mathbb T \)-algebras, denoted \( \mathcal C^{\mathbb T} \).
\end{definition}
\begin{proposition}
    The forgetful functor \( G^{\mathbb T} : \mathcal C^{\mathbb T} \to \mathcal C \) has a left adjoint \( F^{\mathbb T} \), and the adjunction \( F^{\mathbb T} \dashv G^{\mathbb T} \) induces the monad \( \mathbb T \) on \( \mathcal C \).
\end{proposition}
\begin{proof}
    We define the \emph{free algebra} of an object \( A \) to be \( F^{\mathbb T}A = (TA, \mu_A) \).
    This defines an algebra structure on \( TA \) for every \( A \) by the monad laws.
    For \( f : A \to B \), we define \( F^{\mathbb T}f = Tf \); this is a homomorphism by naturality of \( \mu \).
    This is functorial as \( T \) is functorial.

    We have \( G^{\mathbb T} F^{\mathbb T} = T \).
    For the unit of the adjunction, we use the unit of the monad \( \eta \).
    For the counit, we define
    \[ \mu_{(A,\alpha)} = \alpha : F^{\mathbb T} A \to (A, \alpha) \]
    This is a homomorphism by the definition of an algebra, and it is a natural transformation by the definition of homomorphisms of algebras.
    It suffices to verify the triangular identities, which follows from the remaining unused diagrams.
    One can check that the multiplication induced by this monad is equal to that of \( \mathbb T \).
\end{proof}

\subsection{Kleisli categories}
If \( F \dashv G \) with \( F : \mathcal C \to \mathcal D \) and \( G : \mathcal D \to \mathcal C \) is an adjunction inducing \( \mathbb T \), then \( F' \dashv G' \) with \( F' : \mathcal C \to \mathcal D' \) and \( G' : \mathcal D' \to \mathcal C \), where \( \mathcal D' \) is the full subcategory of \( \mathcal D \) on objects in the image of \( F \).
Thus, when finding a construction for \( \mathcal D \), we can assume that \( F \) is surjective (or, indeed, bijective) on objects.
Then, the morphisms \( FA \to FB \) must correspond to morphisms \( A \to GFB \) under the adjunction, but \( GF = T \).
\begin{definition}
    Let \( \mathbb T = (T, \mu, \eta) \) be a monad on \( \mathcal C \).
    The \emph{Kleisli category} \( \mathcal C_{\mathbb T} \) is the category where the objects are precisely the objects of \( \mathcal C \), and the morphisms from \( A \) to \( B \) in \( \mathcal C_{\mathbb T} \) are the morphisms \( A \to TB \) in \( \mathcal C \).
    To avoid confusion, we will denote morphisms from \( A \) to \( B \) in this category by \( A \rightdotarrow B \).
    The identity \( A \rightdotarrow A \) is \( \eta_A : A \to TA \).
    The composite of
    % https://q.uiver.app/#q=WzAsMyxbMCwwLCJBIl0sWzEsMCwiQiJdLFsyLDAsIkMiXSxbMCwxLCJmIiwwLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiZG90dGVkIn19fV0sWzEsMiwiZyIsMCx7InN0eWxlIjp7ImJvZHkiOnsibmFtZSI6ImRvdHRlZCJ9fX1dXQ==
\[\begin{tikzcd}
	A & B & C
	\arrow["f", dotted, from=1-1, to=1-2]
	\arrow["g", dotted, from=1-2, to=1-3]
\end{tikzcd}\]
    is
    % https://q.uiver.app/#q=WzAsNCxbMCwwLCJBIl0sWzEsMCwiVEIiXSxbMiwwLCJUVEMiXSxbMywwLCJUQyJdLFswLDEsImYiXSxbMSwyLCJUZyJdLFsyLDMsIlxcbXVfQyJdXQ==
\[\begin{tikzcd}
	A & TB & T^2C & TC
	\arrow["f", from=1-1, to=1-2]
	\arrow["Tg", from=1-2, to=1-3]
	\arrow["{\mu_C}", from=1-3, to=1-4]
\end{tikzcd}\]
    These satisfy the unit and associativity laws.
    % https://q.uiver.app/#q=WzAsNCxbMCwwLCJBIl0sWzEsMCwiVEIiXSxbMiwwLCJUVEIiXSxbMiwxLCJUQiJdLFswLDEsImYiXSxbMSwyLCJUXFxldGFfQiJdLFsyLDMsIlxcbXVfQiJdLFsxLDMsIjFfe1RCfSJdXQ==
\[\begin{tikzcd}
	A & TB & T^2B \\
	&& TB
	\arrow["f", from=1-1, to=1-2]
	\arrow["{T\eta_B}", from=1-2, to=1-3]
	\arrow["{\mu_B}", from=1-3, to=2-3]
	\arrow["{1_{TB}}"', from=1-2, to=2-3]
\end{tikzcd}\quad\quad\begin{tikzcd}
	A & TA \\
	TB & T^2B \\
	& TB
	\arrow["{\eta_A}", from=1-1, to=1-2]
	\arrow["Tf", from=1-2, to=2-2]
	\arrow["{\mu_B}", from=2-2, to=3-2]
	\arrow["f"', from=1-1, to=2-1]
	\arrow["{\eta_{TB}}", from=2-1, to=2-2]
	\arrow["{1_{TB}}"', from=2-1, to=3-2]
\end{tikzcd}\]
\[\begin{tikzcd}
	A & TB & {T^2C} & {T^3D} & {T^2D} \\
	&& TC & {T^2D} & TD
	\arrow["f", from=1-1, to=1-2]
	\arrow["Tg", from=1-2, to=1-3]
	\arrow["{T^2h}", from=1-3, to=1-4]
	\arrow["{T\mu_D}", from=1-4, to=1-5]
	\arrow["{\mu_D}", from=1-5, to=2-5]
	\arrow["{\mu_{TD}}", from=1-4, to=2-4]
	\arrow["{\mu_D}"', from=2-4, to=2-5]
	\arrow["{\mu_C}", from=1-3, to=2-3]
	\arrow["Th"', from=2-3, to=2-4]
\end{tikzcd}\]
where in the last diagram, the upper composite is \( (hg)f \) and the lower composite is \( h(gf) \) in \( \mathcal C_{\mathbb T} \).
\end{definition}
\begin{proposition}
    There is an adjunction \( F_{\mathbb T} \dashv G_{\mathbb T} \) where \( F_{\mathbb T} : \mathcal C \to \mathcal C_{\mathbb T} \) and \( G_{\mathbb T} : \mathcal C_{\mathbb T} \to \mathcal C \) that induces the monad \( \mathbb T \).
\end{proposition}
\begin{proof}
    We define \( F_{\mathbb T} A = A \), and for \( f : A \to B \), define \( F_{\mathbb T} f = \eta_B f \).
    This preserves identities as \( 1_{F_{\mathbb T} A} = \eta_A \), and preserves composites since% https://q.uiver.app/#q=WzAsNyxbMCwwLCJBIl0sWzEsMCwiQiJdLFsyLDAsIlRCIl0sWzIsMSwiVEMiXSxbMywwLCJUXjJDIl0sWzMsMSwiVEMiXSxbMSwxLCJDIl0sWzAsMSwiZiJdLFsxLDIsIlxcZXRhX0IiXSxbMiwzLCJUZyIsMl0sWzMsNCwiVFxcZXRhX0MiLDFdLFs0LDUsIlxcbXVfQyJdLFszLDUsIjFfe1RDfSIsMl0sWzEsNiwiZyJdLFs2LDMsIlxcZXRhX0MiXV0=
    \[\begin{tikzcd}
        A & B & TB & {T^2C} \\
        & C & TC & TC
        \arrow["f", from=1-1, to=1-2]
        \arrow["{\eta_B}", from=1-2, to=1-3]
        \arrow["Tg"', from=1-3, to=2-3]
        \arrow["{T\eta_C}", from=2-3, to=1-4]
        \arrow["{\mu_C}", from=1-4, to=2-4]
        \arrow["{1_{TC}}"', from=2-3, to=2-4]
        \arrow["g", from=1-2, to=2-2]
        \arrow["{\eta_C}", from=2-2, to=2-3]
    \end{tikzcd}\]
    commutes.
    For \( G_{\mathbb T} \), we define \( G_{\mathbb T} A = TA \), and for \( f : A \rightdotarrow B \), we define \( G_{\mathbb T} f \) to be the composite
    % https://q.uiver.app/#q=WzAsMyxbMCwwLCJUQSJdLFsxLDAsIlRUQiJdLFsyLDAsIlRCIl0sWzAsMSwiVGYiXSxbMSwyLCJcXG11X0IiXV0=
\[\begin{tikzcd}
	TA & T^2B & TB
	\arrow["Tf", from=1-1, to=1-2]
	\arrow["{\mu_B}", from=1-2, to=1-3]
\end{tikzcd}\]
    Note that \( G_{\mathbb T} \) preserves identities by the unit law and preserves composites as
    % https://q.uiver.app/#q=WzAsNyxbMCwwLCJUQSJdLFsxLDAsIlReMkIiXSxbMiwwLCJUXjNDIl0sWzMsMCwiVF4yQyJdLFszLDEsIlRDIl0sWzIsMSwiVF4yQyJdLFsxLDEsIlRCIl0sWzAsMSwiVGYiXSxbMSwyLCJUXjJnIl0sWzIsMywiVFxcbXVfQyJdLFszLDQsIlxcbXVfQyJdLFsyLDUsIlxcbXVfe1RDfSJdLFs1LDQsIlxcbXVfQyIsMl0sWzEsNiwiXFxtdV9CIl0sWzYsNSwiVGciLDJdXQ==
\[\begin{tikzcd}
	TA & {T^2B} & {T^3C} & {T^2C} \\
	& TB & {T^2C} & TC
	\arrow["Tf", from=1-1, to=1-2]
	\arrow["{T^2g}", from=1-2, to=1-3]
	\arrow["{T\mu_C}", from=1-3, to=1-4]
	\arrow["{\mu_C}", from=1-4, to=2-4]
	\arrow["{\mu_{TC}}", from=1-3, to=2-3]
	\arrow["{\mu_C}"', from=2-3, to=2-4]
	\arrow["{\mu_B}", from=1-2, to=2-2]
	\arrow["Tg"', from=2-2, to=2-3]
\end{tikzcd}\]
    commutes.
    Then \( G_{\mathbb T} \) is a functor, and \( G_{\mathbb T} F_{\mathbb T} = T \).
    The unit of the adjunction is the unit of the monad \( \eta \).
    For the counit \( \epsilon_A : TA = F_{\mathbb T} G_{\mathbb T} A \rightdotarrow A \), we use the identity \( 1_{TA} \).
    This is natural, as given \( f : A \rightdotarrow B \), the diagram
    % https://q.uiver.app/#q=WzAsNCxbMCwwLCJUQSJdLFsxLDAsIlRCIl0sWzEsMSwiQiJdLFswLDEsIkEiXSxbMCwxLCJGX3tcXG1hdGhiYiBUfSBHX3tcXG1hdGhiYiBUfWYiLDAseyJzdHlsZSI6eyJib2R5Ijp7Im5hbWUiOiJkb3R0ZWQifX19XSxbMSwyLCJcXGVwc2lsb25fQiIsMCx7InN0eWxlIjp7ImJvZHkiOnsibmFtZSI6ImRvdHRlZCJ9fX1dLFswLDMsIlxcZXBzaWxvbl9BIiwyLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiZG90dGVkIn19fV0sWzMsMiwiZiIsMix7InN0eWxlIjp7ImJvZHkiOnsibmFtZSI6ImRvdHRlZCJ9fX1dXQ==
\[\begin{tikzcd}[column sep=large]
	TA & TB \\
	A & B
	\arrow["{F_{\mathbb T} G_{\mathbb T}f}", dotted, from=1-1, to=1-2]
	\arrow["{\epsilon_B}", dotted, from=1-2, to=2-2]
	\arrow["{\epsilon_A}"', dotted, from=1-1, to=2-1]
	\arrow["f"', dotted, from=2-1, to=2-2]
\end{tikzcd}\]
    commutes, as the paths are% https://q.uiver.app/#q=WzAsNSxbMCwwLCJUQSJdLFsxLDAsIlReMkIiXSxbMiwwLCJUQiJdLFszLDAsIlReMkIiXSxbNCwwLCJUQiJdLFswLDEsIlRmIl0sWzEsMiwiXFxtdV9CIl0sWzIsMywiXFxldGFfe1RCfSJdLFszLDQsIlxcbXVfQiJdXQ==
    \[\begin{tikzcd}
        TA & {T^2B} & TB & {T^2B} & TB
        \arrow["Tf", from=1-1, to=1-2]
        \arrow["{\mu_B}", from=1-2, to=1-3]
        \arrow["{\eta_{TB}}", from=1-3, to=1-4]
        \arrow["{\mu_B}", from=1-4, to=1-5]
    \end{tikzcd}\]
    and
    % https://q.uiver.app/#q=WzAsMyxbMCwwLCJUQSJdLFsxLDAsIlReMkIiXSxbMiwwLCJUQiJdLFswLDEsIlRmIl0sWzEsMiwiXFxtdV9CIl1d
\[\begin{tikzcd}
	TA & {T^2B} & TB
	\arrow["Tf", from=1-1, to=1-2]
	\arrow["{\mu_B}", from=1-2, to=1-3]
\end{tikzcd}\]
    which coincide.
    One can show that both triangular identities reduce to a unit law.
    It suffices to verify that the multiplication of the induced monad is correct.
    The multiplication law is \( G_{\mathbb T} \epsilon_{F_{\mathbb T} A} \), which is
    % https://q.uiver.app/#q=WzAsMyxbMCwwLCJUXjJBIl0sWzEsMCwiVF4yQSJdLFsyLDAsIlRBIl0sWzAsMSwiVDFfe1RBfSJdLFsxLDIsIlxcbXVfQSJdXQ==
\[\begin{tikzcd}
	{T^2A} & {T^2A} & TA
	\arrow["{T1_{TA}}", from=1-1, to=1-2]
	\arrow["{\mu_A}", from=1-2, to=1-3]
\end{tikzcd}\]
    which is equal to \( \mu_A \), as required.
\end{proof}

\subsection{Comparison functors}
\begin{definition}
    Let \( \mathbb T = (T, \eta, \mu) \) be a monad on \( \mathcal C \).
    Then \( \operatorname{Adj}(\mathbb T) \) is the category of adjunctions \( F \dashv G \) which induce \( \mathbb T \), where the morphisms \( F \dashv G \) to \( F' \dashv G' \) are the functors \( K : \mathcal D \to \mathcal D' \) satisfying \( KF = F' \) and \( G' K = G \).
\end{definition}
\begin{theorem}
    The Kleisli adjunction \( F_{\mathbb T} \dashv G_{\mathbb T} \) is initial in \( \operatorname{Adj}(\mathbb T) \), and the Eilenberg--Moore adjunction \( F^{\mathbb T} \dashv G^{\mathbb T} \) is terminal in \( \operatorname{Adj}(\mathbb T) \).
\end{theorem}
% TODO: Define the comparison functors
\begin{proof}
    We will first do the case of the Eilenberg--Moore adjunction.
    Let \( F \dashv G \) be an adjunction inducing \( \mathbb T \).
    We define \( K : \mathcal D \to \mathcal C^{\mathbb T} \) by \( KB = (GB, G\epsilon_B) \).
    This is an algebra by the triangular identities and naturality of \( \epsilon \).
    On morphisms \( f : B \to C \) in \( \mathcal D \), we define \( Kg = Gg \), which is a homomorphism as \( \epsilon \) is a natural transformation.
    Clearly \( G^{\mathbb T}K = G \), and \( KFA = (GFA, G\epsilon_{FA}) = F^{\mathbb T}A \), and for \( f : A \to A' \), \( KFf = GFf = Tf = F^{\mathbb T} f \).
    So \( K \) is a morphism of \( \operatorname{Adj}(\mathbb T) \).

    For uniqueness, suppose \( K' \) were another such morphism.
    Then \( K'B = (GB, \beta_B) \), and \( K'g = Gg \) for \( g : B \to C \).
    Note that \( \beta \) must be a natural transformation \( GFG \to G \).
    Also, \( \beta_{FA} = G\epsilon_{FA} \) for all \( A \), as \( K'F = F^{\mathbb T} \).
    But we have naturality squares
    % https://q.uiver.app/#q=WzAsNCxbMCwwLCJHRkdGR0IiXSxbMCwxLCJHRkdCIl0sWzEsMCwiR0ZHQiJdLFsxLDEsIkdCIl0sWzAsMSwiXFxiZXRhX3tGR0J9IiwyLHsib2Zmc2V0IjoyfV0sWzAsMiwiR0ZHXFxlcHNpbG9uX0IiXSxbMSwzLCJHXFxlcHNpbG9uX0IiLDJdLFswLDEsIkdcXGVwc2lsb25fe0ZHQn0iLDAseyJvZmZzZXQiOi0yfV0sWzIsMywiXFxiZXRhX0IiLDIseyJvZmZzZXQiOjJ9XSxbMiwzLCJHXFxlcHNpbG9uX0IiLDAseyJvZmZzZXQiOi0yfV1d
\[\begin{tikzcd}[column sep=large]
	GFGFGB & GFGB \\
	GFGB & GB
	\arrow["{\beta_{FGB}}"', shift right=2, from=1-1, to=2-1]
	\arrow["{GFG\epsilon_B}", from=1-1, to=1-2]
	\arrow["{G\epsilon_B}"', from=2-1, to=2-2]
	\arrow["{G\epsilon_{FGB}}", shift left=2, from=1-1, to=2-1]
	\arrow["{\beta_B}"', shift right=2, from=1-2, to=2-2]
	\arrow["{G\epsilon_B}", shift left=2, from=1-2, to=2-2]
\end{tikzcd}\]
    where the left edges are equal and the top edge is a split epimorphism, so the right edges are equal.
    Thus \( K \) is unique.

    Given an adjunction \( F \dashv G \) inducing \( \mathbb T \), we define \( H : \mathcal C_{\mathbb T} \to \mathcal D \) by \( HA = FA \), and for \( f : A \rightdotarrow B \), define \( Hf \) to be the composite
    % https://q.uiver.app/#q=WzAsMyxbMCwwLCJGQSJdLFsxLDAsIkZHRkIiXSxbMiwwLCJGQiJdLFswLDEsIkZmIl0sWzEsMiwiXFxlcHNpbG9uX3tGQn0iXV0=
\[\begin{tikzcd}
	FA & FGFB & FB
	\arrow["Ff", from=1-1, to=1-2]
	\arrow["{\epsilon_{FB}}", from=1-2, to=1-3]
\end{tikzcd}\]
This is functorial.
Indeed, for \( f : A \rightdotarrow B \) and \( g : B \rightdotarrow C \), \( H(gf) \) is the upper composite and \( (Hg)(Hf) \) is the lower composite in the following diagram.
    % https://q.uiver.app/#q=WzAsNyxbMCwwLCJGQSJdLFsxLDAsIkZHRkIiXSxbMiwwLCJGR0ZHRkMiXSxbMywwLCJGR0ZDIl0sWzMsMSwiRkMiXSxbMiwxLCJGR0ZDIl0sWzEsMSwiRkIiXSxbMCwxLCJGZiJdLFsxLDIsIkZHRmciXSxbMiwzLCJGR1xcZXBzaWxvbl97RkN9Il0sWzMsNCwiXFxlcHNpbG9uX3tGQ30iXSxbMiw1LCJcXGVwc2lsb25fe0ZHRkN9Il0sWzUsNCwiXFxlcHNpbG9uX3tGQ30iLDJdLFsxLDYsIlxcZXBzaWxvbl97RkJ9Il0sWzYsNSwiRmciLDJdXQ==
\[\begin{tikzcd}[column sep=large]
	FA & FGFB & FGFGFC & FGFC \\
	& FB & FGFC & FC
	\arrow["Ff", from=1-1, to=1-2]
	\arrow["FGFg", from=1-2, to=1-3]
	\arrow["{FG\epsilon_{FC}}", from=1-3, to=1-4]
	\arrow["{\epsilon_{FC}}", from=1-4, to=2-4]
	\arrow["{\epsilon_{FGFC}}", from=1-3, to=2-3]
	\arrow["{\epsilon_{FC}}"', from=2-3, to=2-4]
	\arrow["{\epsilon_{FB}}", from=1-2, to=2-2]
	\arrow["Fg"', from=2-2, to=2-3]
\end{tikzcd}\]
    Then \( HF_{\mathbb T}(f) = \epsilon_{FB} (F\eta_B) (Ff) = Ff \).
    Moreover, \( GHA = GFA = TA = G_{\mathbb T} A \), and for \( f : A \rightdotarrow B \), \( GFf \) is the composite
    % https://q.uiver.app/#q=WzAsMyxbMCwwLCJHRkEiXSxbMSwwLCJHRkdGQiJdLFsyLDAsIkdGQiJdLFswLDEsIkdGZiJdLFsxLDIsIlxcbXVfQiJdXQ==
\[\begin{tikzcd}
	GFA & GFGFB & GFB
	\arrow["GFf", from=1-1, to=1-2]
	\arrow["{\mu_B}", from=1-2, to=1-3]
\end{tikzcd}\]
    which is the definition of \( G_{\mathbb T}(f) \).
    Thus \( H \) is a morphism of \( \operatorname{Adj}(\mathbb T) \).
    If \( H' : \mathcal C_{\mathbb T} \to \mathcal D \) were another such morphism, then since \( H' F_{\mathbb T} = F \), we must have \( H' A = FA \) for all \( A \).
    Note that for \( f : A \rightdotarrow B \), \( Hf \) is the transpose of \( f : A \to GFB \) across \( F \dashv G \).
    Since \( H' \) commutes with \( G \) and \( G_{\mathbb T} \), and \( F \dashv G \) and \( F_{\mathbb T} \dashv G_{\mathbb T} \) have the same unit \( \eta \), \( H' \) must send the transpose \( f : A \rightdotarrow B \) of \( f : A \to GFB \) to its transpose across \( F \dashv G \), which is precisely the action of \( H \) on morphisms.
    Hence \( H' = H \).
\end{proof}
\begin{definition}
    The functor \( K : \mathcal D \to \mathcal C^{\mathbb T} \) is called the \emph{Eilenberg--Moore comparison functor}.
    Similarly, the functor \( H : \mathcal C_{\mathbb T} \to \mathcal D \) is called the \emph{Kleisli comparison functor}.
\end{definition}
\begin{remark}
    Note that \( \mathcal C_{\mathbb T} \) has coproducts if \( \mathcal C \) does, since \( F_{\mathbb T} \) preserves them and is bijective on objects.
    However, it has few other limits or colimits in general.
    In contrast, \( \mathcal C^{\mathbb T} \) inherits many limits and colimits from \( \mathcal C \).
\end{remark}
\begin{proposition}
    \begin{enumerate}
        \item The forgetful functor \( G = G^{\mathbb T} : \mathcal C^{\mathbb T} \to \mathcal C \) creates any limits which exist in \( \mathcal C \).
        \item If \( \mathcal C \) has colimits of shape \( J \), then \( G = G^{\mathbb T} \) creates colimits of shape \( J \) if and only if \( T \) preserves them.
    \end{enumerate}
\end{proposition}
\begin{proof}
    \emph{Part (i).}
    Let \( D : J \to \mathcal C^{\mathbb T} \) be a diagram of shape \( J \).
    Write \( D(j) = (GD(j), \delta_j) \) for \( j \in \ob J \).
    Let \( (L, (\lambda_j : L \to GD(j))_{j \in \ob J}) \) be a limit for \( GD \) in \( \mathcal C \).
    Then \( (TL, (T\lambda_j)_{j \in \ob J}) \) is a cone over \( TGD \), so \( (TL, (\delta(T\lambda_j))_{j \in \ob J}) \) is a cone over \( TGD \), and induces a unique \( \theta : TL \to L \) making squares of the form
    % TODO: is it really TGD above?
    % https://q.uiver.app/#q=WzAsNCxbMCwwLCJUTCJdLFsxLDAsIlRHRChqKSJdLFsxLDEsIkdEKGopIl0sWzAsMSwiTCJdLFswLDEsIlRcXGxhbWJkYV9qIl0sWzEsMiwiXFxkZWx0YV9qIl0sWzAsMywiXFx0aGV0YSIsMl0sWzMsMiwiXFxsYW1iZGFfaiIsMl1d
\[\begin{tikzcd}
	TL & {TGD(j)} \\
	L & {GD(j)}
	\arrow["{T\lambda_j}", from=1-1, to=1-2]
	\arrow["{\delta_j}", from=1-2, to=2-2]
	\arrow["\theta"', from=1-1, to=2-1]
	\arrow["{\lambda_j}"', from=2-1, to=2-2]
\end{tikzcd}\]
    commute for each \( j \).
    Note that \( \theta \) is an algebra structure on \( L \), since the required diagrams commute by uniqueness of factorisation through limits.
    It is the unique algebra structure on \( L \) which make the \( \lambda_j \) into a cone in \( \mathcal C^{\mathbb T} \), and one can easily show it is a limit cone.

    \emph{Part (ii).}
    In the forward direction, if \( G \) creates colimits of shape \( J \), then it certainly preserves them, as they exist in both categories.
    But \( F \) preserves all colimits, so \( T = GF \) preserves them.
    Given \( D : J \to \mathcal C^{\mathbb T} \) and a colimit cone \( \lambda_j : GD(j) \to L \) under \( GD \), we know that \( T\lambda_j : TGD(j) \to TL \) is a colimit cone, so there is a unique \( \theta : TL \to L \) satisfying \( \theta(T\lambda_j) = \lambda_j \delta_j \) for all \( j \), and \( \theta \) is an algebra structure since \( TTL \) is also a colimit.
    Hence \( (L, \theta) \) is a colimit for \( D \) in \( \mathcal C^{\mathbb T} \).
\end{proof}
\begin{remark}
    One can show that \( \mathcal C^{\mathbb T} \) has colimits of any shape which exist in \( \mathcal C \), provided that it has \emph{reflexive coequalisers}.
\end{remark}

\subsection{Monadic adjunctions}
It can be useful to know, for an arbitrary adjunction, if the Eilenberg--Moore comparison functor \( K : \mathcal D \to \mathcal C^{\mathbb T} \) is part of an equivalence of categories.
Note that the Kleisli comparison functor \( H \) is always full and faithful, so is part of an equivalence if and only if it is essentially surjective, and since its action on objects is \( F \), this holds if and only if \( F \) is essentially surjective.
\begin{definition}
    An adjunction \( F \dashv G \) is \emph{monadic}, or the right adjoint \( G \) is \emph{monadic}, if \( K \) is part of an equivalence.
\end{definition}
\begin{lemma}
    Let \( F \dashv G \) be an adjunction inducing the monad \( \mathbb T \), and suppose that for every \( \mathbb T \)-algebra \( (A, \alpha) \), the pair
    % https://q.uiver.app/#q=WzAsMixbMCwwLCJGR0ZBIl0sWzEsMCwiRkEiXSxbMCwxLCJGXFxhbHBoYSIsMCx7Im9mZnNldCI6LTJ9XSxbMCwxLCJcXGVwc2lsb25fe0ZBfSIsMix7Im9mZnNldCI6Mn1dXQ==
\[\begin{tikzcd}
	FGFA & FA
	\arrow["F\alpha", shift left=2, from=1-1, to=1-2]
	\arrow["{\epsilon_{FA}}"', shift right=2, from=1-1, to=1-2]
\end{tikzcd}\]
    has a coequaliser in \( \mathcal D \).
    Then the comparison functor \( K : \mathcal D \to \mathcal C^{\mathbb T} \) has a left adjoint \( L \).
\end{lemma}
\begin{proof}
    Let \( \lambda_{(A, \alpha)} : FA \to L(A, \alpha) \) be a coequaliser for \( F\alpha, \epsilon_{FA} \).
    We can make \( L \) into a functor \( \mathcal C^{\mathbb T} \to \mathcal D \).
    Given \( f : (A, \alpha) \to (B, \beta) \), the composite \( \lambda_{(B, \beta)} (Ff) \) coequalises \( F\alpha \) and \( \epsilon_{FA} \), so it induces a unique map \( Lf : L(A, \alpha) \to L(B, \beta) \).
    This makes \( L \) into a functor by uniqueness.
% https://q.uiver.app/#q=WzAsNixbMCwwLCJGR0ZBIl0sWzEsMCwiRkEiXSxbMiwwLCJMKEEsIFxcYWxwaGEpIl0sWzAsMSwiRkdGQiJdLFsxLDEsIkZCIl0sWzIsMSwiTChCLFxcYmV0YSkiXSxbMCwxLCJGXFxhbHBoYSIsMCx7Im9mZnNldCI6LTJ9XSxbMSwyLCJcXGxhbWJkYV97KEEsXFxhbHBoYSl9Il0sWzMsNCwiRlxcYmV0YSIsMCx7Im9mZnNldCI6LTJ9XSxbNCw1LCJcXGxhbWJkYV97KEIsIFxcYmV0YSl9IiwyXSxbMSw0LCJGZiJdLFsyLDUsIkxmIl0sWzAsMSwiXFxlcHNpbG9uX3tGQX0iLDIseyJvZmZzZXQiOjJ9XSxbMyw0LCJcXGVwc2lsb25fe0ZCfSIsMix7Im9mZnNldCI6MX1dLFswLDMsIkZHRmYiLDJdXQ==
\[\begin{tikzcd}
	FGFA & FA & {L(A, \alpha)} \\
	FGFB & FB & {L(B,\beta)}
	\arrow["F\alpha", shift left=2, from=1-1, to=1-2]
	\arrow["{\lambda_{(A,\alpha)}}", from=1-2, to=1-3]
	\arrow["F\beta", shift left=2, from=2-1, to=2-2]
	\arrow["{\lambda_{(B, \beta)}}"', from=2-2, to=2-3]
	\arrow["Ff", from=1-2, to=2-2]
	\arrow["Lf", from=1-3, to=2-3]
	\arrow["{\epsilon_{FA}}"', shift right=2, from=1-1, to=1-2]
	\arrow["{\epsilon_{FB}}"', shift right, from=2-1, to=2-2]
	\arrow["FGFf"', from=1-1, to=2-1]
\end{tikzcd}\]
    For any object \( B \) of \( \mathcal D \), morphisms \( L(A, \alpha) \to B \) correspond to morphisms \( f : FA \to B \) satisfying \( f(F\alpha) = f \epsilon_{FA} \).
    If \( \overline f : A \to GB \) is the transpose of \( f \) across \( F \dashv G \), then by naturality, the transpose of \( f(F\alpha) \) is \( \overline f \alpha \), and the transpose of \( f \epsilon_{FA} \) is \( Gf \) since \( \epsilon_{FA} \) transposes to \( 1_{GFA} \).
    But we have \( f = \epsilon_B (F\overline f) \), so \( (G \epsilon_B)(GF \overline f) = (G\epsilon_B)(T\overline f) \).
    Thus \( f(F\alpha) = f(\epsilon_{FA}) \) if and only if \( \overline f \alpha = (G\epsilon_B)(T \overline f) \), which is to say that \( \overline f \) is an algebra homomorphism \( (A, \alpha) \to (GB, G\epsilon_B) = KB \).
    Naturality of this bijection follows from the fact that the map \( f \mapsto \overline f \) is natural, so \( L \dashv K \) as required.
\end{proof}
\begin{definition}
    A parallel pair \( f, g : A \rightrightarrows B \) is \emph{reflexive} if there exists \( r : B \to A \) such that \( fr = gr = 1_B \).
    % https://q.uiver.app/#q=WzAsMyxbMCwxLCJCIl0sWzAsMCwiQSJdLFsxLDAsIkIiXSxbMCwxLCJyIl0sWzEsMiwiZiIsMCx7Im9mZnNldCI6LTJ9XSxbMSwyLCJnIiwyLHsib2Zmc2V0IjoyfV0sWzAsMiwiMV9CIiwyLHsiY3VydmUiOjJ9XV0=
\[\begin{tikzcd}
	A & B \\
	B
	\arrow["r", from=2-1, to=1-1]
	\arrow["f", shift left=2, from=1-1, to=1-2]
	\arrow["g"', shift right=2, from=1-1, to=1-2]
	\arrow["{1_B}"', curve={height=12pt}, from=2-1, to=1-2]
\end{tikzcd}\]
\end{definition}
Note that the parallel pair
\[\begin{tikzcd}
	FGFA & FA
	\arrow["F\alpha", shift left=2, from=1-1, to=1-2]
	\arrow["{\epsilon_{FA}}"', shift right=2, from=1-1, to=1-2]
\end{tikzcd}\]
is a reflexive pair, and the common right inverse is \( r = F \eta_A \).
\begin{definition}
    A \emph{split coequaliser diagram} is a diagram
    % https://q.uiver.app/#q=WzAsMyxbMCwwLCJBIl0sWzEsMCwiQiJdLFsyLDAsIkMiXSxbMCwxLCJmIiwwLHsib2Zmc2V0IjotNH1dLFsxLDIsImgiLDAseyJvZmZzZXQiOi0yfV0sWzAsMSwiZyIsMl0sWzEsMCwidCIsMCx7Im9mZnNldCI6LTIsImN1cnZlIjotMn1dLFsyLDEsInMiLDAseyJjdXJ2ZSI6LTJ9XV0=
\[\begin{tikzcd}[column sep=large]
	A & B & C
	\arrow["f", shift left=4, from=1-1, to=1-2]
	\arrow["h", shift left=2, from=1-2, to=1-3]
	\arrow["g"', from=1-1, to=1-2]
	\arrow["t", shift left=2, curve={height=-12pt}, from=1-2, to=1-1]
	\arrow["s", curve={height=-12pt}, from=1-3, to=1-2]
\end{tikzcd}\]
    such that \( hf = hg, hs = 1_C, gt = 1_B, ft = sh \).
    That is, \( h \) equalises \( f \) and \( g \), and the following diagrams commute.
    % https://q.uiver.app/#q=WzAsNSxbMCwwLCJBIl0sWzEsMCwiQiJdLFsyLDAsIkMiXSxbMSwxLCJDIl0sWzAsMSwiQiJdLFswLDEsImciXSxbMSwyLCJoIl0sWzMsMSwicyIsMl0sWzMsMiwiMV9DIiwyXSxbNCwwLCJ0Il0sWzQsMSwiMV9CIiwyXV0=
\[\begin{tikzcd}
	A & B & C \\
	B & C
	\arrow["g", from=1-1, to=1-2]
	\arrow["h", from=1-2, to=1-3]
	\arrow["s"', from=2-2, to=1-2]
	\arrow["{1_C}"', from=2-2, to=1-3]
	\arrow["t", from=2-1, to=1-1]
	\arrow["{1_B}"', from=2-1, to=1-2]
\end{tikzcd}\quad\quad\begin{tikzcd}
	B & A \\
	C & B
	\arrow["f", from=1-2, to=2-2]
	\arrow["t", from=1-1, to=1-2]
	\arrow["h"', from=1-1, to=2-1]
	\arrow["s"', from=2-1, to=2-2]
\end{tikzcd}\]
\end{definition}
The equations \( hs = 1_C, gt = 1_B \) enforce that \( s \) is a section of \( h \), and \( t \) is a section of \( g \).
The equation \( ft = sh \) enforces that the two non-identity paths from \( B \) to itself coincide.

Note that this implies that \( h \) is a coequaliser of \( f \) and \( g \).
Indeed, if \( k : B \to D \) satisfies \( kf = kg \), then \( k = kgt = kft = ksh \), so \( k \) factors through \( h \).
Moreover, this factorisation is unique as \( h \) is split epic.
Any functor preserves split coequaliser diagrams.
\begin{definition}
    Given a functor \( G : \mathcal D \to \mathcal C \), we say that a parallel pair \( f, g : A \rightrightarrows B \) in \( \mathcal D \) is \emph{\( G \)-split} if there is a split coequaliser diagram
    % https://q.uiver.app/#q=WzAsMyxbMCwwLCJHQSJdLFsxLDAsIkdCIl0sWzIsMCwiQyJdLFswLDEsIkdmIiwwLHsib2Zmc2V0IjotNH1dLFsxLDIsImgiLDAseyJvZmZzZXQiOi0yfV0sWzAsMSwiR2ciLDJdLFsxLDAsInQiLDAseyJvZmZzZXQiOi0yLCJjdXJ2ZSI6LTJ9XSxbMiwxLCJzIiwwLHsiY3VydmUiOi0yfV1d
\[\begin{tikzcd}[column sep=large]
	GA & GB & C
	\arrow["Gf", shift left=4, from=1-1, to=1-2]
	\arrow["h", shift left=2, from=1-2, to=1-3]
	\arrow["Gg"', from=1-1, to=1-2]
	\arrow["t", shift left=2, curve={height=-12pt}, from=1-2, to=1-1]
	\arrow["s", curve={height=-12pt}, from=1-3, to=1-2]
\end{tikzcd}\]
    in \( \mathcal C \).
\end{definition}
Note that the pair
\[\begin{tikzcd}
	FGFA & FA
	\arrow["F\alpha", shift left=2, from=1-1, to=1-2]
	\arrow["{\epsilon_{FA}}"', shift right=2, from=1-1, to=1-2]
\end{tikzcd}\]
is \( G \)-split, as
% https://q.uiver.app/#q=WzAsMyxbMCwwLCJHRkdGQSJdLFsxLDAsIkdGQSJdLFsyLDAsIkMiXSxbMCwxLCJHRlxcYWxwaGEiLDAseyJvZmZzZXQiOi00fV0sWzEsMiwiXFxhbHBoYSIsMCx7Im9mZnNldCI6LTJ9XSxbMCwxLCJHXFxlcHNpbG9uX3tGQX09XFxtdV9BIiwyXSxbMSwwLCJcXGV0YV97R0ZBfSIsMCx7Im9mZnNldCI6LTIsImN1cnZlIjotMn1dLFsyLDEsIlxcZXRhX0EiLDAseyJjdXJ2ZSI6LTJ9XV0=
\[\begin{tikzcd}[column sep=huge]
	GFGFA & GFA & C
	\arrow["GF\alpha", shift left=4, from=1-1, to=1-2]
	\arrow["\alpha", shift left=2, from=1-2, to=1-3]
	\arrow["{G\epsilon_{FA}=\mu_A}"', from=1-1, to=1-2]
	\arrow["{\eta_{GFA}}", shift left=2, curve={height=-12pt}, from=1-2, to=1-1]
	\arrow["{\eta_A}", curve={height=-12pt}, from=1-3, to=1-2]
\end{tikzcd}\]
is a split coequaliser diagram.
\begin{theorem}[Beck's precise monadicity theorem]
    A functor \( G : \mathcal D \to \mathcal C \) is monadic if and only if \( G \) has a left adjoint and creates coequalisers of \( G \)-split pairs.
\end{theorem}
\begin{theorem}[Beck's crude monadicity theorem]
    Suppose \( G : \mathcal D \to \mathcal C \) has a left adjoint, and \( G \) reflects isomorphisms.
    Suppose further that \( \mathcal D \) has and \( G \) preserves reflexive coequalisers.
    Then \( G \) is monadic.
\end{theorem}
We prove both theorems together.
\begin{proof}
    First, suppose \( G : \mathcal D \to \mathcal C \) is monadic.
    Then \( G \) has a left adjoint by definition.
    It suffices to show that \( G^{\mathbb T} : \mathcal C^{\mathbb T} \to \mathcal C \) creates coequalisers of \( G^{\mathbb T} \)-split pairs.
    This follows from the argument of a previous lemma: if \( f, g : (A, \alpha) \rightrightarrows (B, \beta) \) are algebra homomorphisms, and
        % https://q.uiver.app/#q=WzAsMyxbMCwwLCJBIl0sWzEsMCwiQiJdLFsyLDAsIkMiXSxbMCwxLCJmIiwwLHsib2Zmc2V0IjotNH1dLFsxLDIsImgiLDAseyJvZmZzZXQiOi0yfV0sWzAsMSwiZyIsMl0sWzEsMCwidCIsMCx7Im9mZnNldCI6LTIsImN1cnZlIjotMn1dLFsyLDEsInMiLDAseyJjdXJ2ZSI6LTJ9XV0=
\[\begin{tikzcd}[column sep=large]
	A & B & C
	\arrow["f", shift left=4, from=1-1, to=1-2]
	\arrow["h", shift left=2, from=1-2, to=1-3]
	\arrow["g"', from=1-1, to=1-2]
	\arrow["t", shift left=2, curve={height=-12pt}, from=1-2, to=1-1]
	\arrow["s", curve={height=-12pt}, from=1-3, to=1-2]
\end{tikzcd}\]
    is a split coequaliser, then since the coequaliser is preserved by \( T \) and \( T^2 \), \( C \) acquires a unique algebra structure \( \gamma : TC \to C \) such that \( h \) is a coequaliser in \( \mathcal C^{\mathbb T} \).
    % ^ = lemma 5.8(ii)

    For the converse, either set of assumptions ensures that \( \mathcal D \) has coequalisers of parallel pairs of the form
    \[\begin{tikzcd}
        FGFA & FA
        \arrow["F\alpha", shift left=2, from=1-1, to=1-2]
        \arrow["{\epsilon_{FA}}"', shift right=2, from=1-1, to=1-2]
    \end{tikzcd}\]
    so the comparison functor \( K : \mathcal D \to \mathcal C^{\mathbb T} \) has a left adjoint \( L \).
    We must now show that the unit and counit of \( L \dashv K \) are isomorphisms.
    The unit \( (A, \alpha) \to KL(A, \alpha) \) is the unique factorisation of \( G\lambda_{(A, \alpha)} : GFA \to GL(A, \alpha) \) through the (\( G^{\mathbb T} \)-split) coequaliser \( \alpha : GFA \to A \) of \( GF\alpha, G\epsilon_{FA} : GFGFA \rightrightarrows GFA \) in \( \mathcal C^{\mathbb T} \).
    But either set of hypotheses implies that \( G \) preserves the coequaliser of \( F\alpha, \epsilon_{FA} \), so the factorisation is an isomorphism.
    The counit \( LKB \to B \) is the unique factorisation of \( \epsilon_B : FGB \to B \) through \( \lambda_{KB} : FGB \to LKB \).
    The hypothesis in the precise theorem implies directly that \( \epsilon_B \) is a coequaliser of \( FG\epsilon_B, \epsilon_{GFB} \), because the pair is \( G \)-split.
    From the hypotheses of the crude theorem, we can see that both \( \epsilon_B \) and \( \lambda_{KB} \) map to coequalisers in \( \mathcal C \), so the counit maps to an isomorphism in \( \mathcal C \), so it is an isomorphism as \( G \) reflects isomorphisms.
\end{proof}
\begin{remark}
    \begin{enumerate}
        \item Let \( J \) be the finite category
        % https://q.uiver.app/#q=WzAsMixbMCwwLCJBIl0sWzEsMCwiQiJdLFswLDEsImYiLDAseyJvZmZzZXQiOi00fV0sWzAsMSwiZyIsMix7Im9mZnNldCI6NH1dLFsxLDAsInIiLDFdXQ==
\[\begin{tikzcd}
	\arrow[loop above]{s}{s} \arrow[loop below]{t}{t} A & B
	\arrow["f", shift left=4, from=1-1, to=1-2]
	\arrow["g"', shift right=4, from=1-1, to=1-2]
	\arrow["r"{description}, from=1-2, to=1-1]
\end{tikzcd}\]
        % TODO: Loops s, t on A
        with \( fr = gr = 1_B, rf = s, rg = t \), then a diagram \( D \) of this shape is a reflexive pair.
        A cone under it is determined by \( h : DB \to L \), which must satisfy \( h(Df) = h(Dg) \).
        A colimit for this diagram is a coequaliser for \( f, g \).
        \item All small (respectively finite) colimits can be constructed from small (respectively finite) coproducts and reflexive coequalisers.
        The pair \( f, g : P \rightrightarrows Q \) in the proof form a coreflexive pair, with common left inverse \( r : Q \to P \) given by \( \pi_j r = \pi_{1_j} \) for all \( j \).
        \item Given a reflexive pair \( f, g : A \rightrightarrows B \), a morphism \( h : B \to C \) is a coequaliser for it if and only if the diagram
        % https://q.uiver.app/#q=WzAsNCxbMCwwLCJBIl0sWzEsMCwiQiJdLFsxLDEsIkMiXSxbMCwxLCJCIl0sWzAsMSwiZiJdLFsxLDIsImgiXSxbMCwzLCJnIiwyXSxbMywyLCJoIiwyXV0=
        \[\begin{tikzcd}
            A & B \\
            B & C
            \arrow["f", from=1-1, to=1-2]
            \arrow["h", from=1-2, to=2-2]
            \arrow["g"', from=1-1, to=2-1]
            \arrow["h"', from=2-1, to=2-2]
        \end{tikzcd}\]
        is a pushout, since any cone under the span given by \( f \) and \( g \) has its two legs equal.
        The dual of this statement has already been proven.
        \item In any cartesian closed category, reflexive coequalisers commute with finite products: if the following are reflexive coequaliser diagrams,
        % https://q.uiver.app/#q=WzAsMyxbMCwwLCJBXzEiXSxbMSwwLCJCXzEiXSxbMiwwLCJDXzEiXSxbMCwxLCJmXzEiLDAseyJvZmZzZXQiOi0yfV0sWzEsMiwiaF8xIl0sWzAsMSwiZ18xIiwyLHsib2Zmc2V0IjoyfV1d
\[\begin{tikzcd}
	{A_1} & {B_1} & {C_1}
	\arrow["{f_1}", shift left=2, from=1-1, to=1-2]
	\arrow["{h_1}", from=1-2, to=1-3]
	\arrow["{g_1}"', shift right=2, from=1-1, to=1-2]
\end{tikzcd}\quad\quad\begin{tikzcd}
	{A_2} & {B_2} & {C_2}
	\arrow["{f_2}", shift left=2, from=1-1, to=1-2]
	\arrow["{h_2}", from=1-2, to=1-3]
	\arrow["{g_2}"', shift right=2, from=1-1, to=1-2]
\end{tikzcd}\]
        then the following diagram is also a coequaliser.
        % https://q.uiver.app/#q=WzAsMyxbMSwwLCJCXzEgXFx0aW1lcyBCXzIiXSxbMiwwLCJDXzEgXFx0aW1lcyBDXzIiXSxbMCwwLCJBXzEgXFx0aW1lcyBBXzIiXSxbMCwxLCJoXzEgXFx0aW1lcyBoXzIiXSxbMiwwLCJmXzEgXFx0aW1lcyBmXzIiLDAseyJvZmZzZXQiOi0yfV0sWzIsMCwiZ18xIFxcdGltZXMgZ18yIiwyLHsib2Zmc2V0IjoyfV1d
\[\begin{tikzcd}[column sep=large]
	{A_1 \times A_2} & {B_1 \times B_2} & {C_1 \times C_2}
	\arrow["{h_1 \times h_2}", from=1-2, to=1-3]
	\arrow["{f_1 \times f_2}", shift left=2, from=1-1, to=1-2]
	\arrow["{g_1 \times g_2}"', shift right=2, from=1-1, to=1-2]
\end{tikzcd}\]
        Indeed, consider the diagram
        % https://q.uiver.app/#q=WzAsOSxbMSwwLCJCXzEgXFx0aW1lcyBBXzIiXSxbMiwwLCJDXzEgXFx0aW1lcyBBXzIiXSxbMCwwLCJBXzEgXFx0aW1lcyBBXzIiXSxbMCwxLCJBXzEgXFx0aW1lcyBCXzIiXSxbMSwxLCJCXzEgXFx0aW1lcyBCXzIiXSxbMiwxLCJDXzEgXFx0aW1lcyBCXzIiXSxbMCwyLCJBXzEgXFx0aW1lcyBDXzIiXSxbMSwyLCJCXzEgXFx0aW1lcyBDXzIiXSxbMiwyLCJDXzEgXFx0aW1lcyBDXzIiXSxbMCwxXSxbMiwwLCIiLDAseyJvZmZzZXQiOi0yfV0sWzIsMCwiIiwyLHsib2Zmc2V0IjoyfV0sWzIsMywiIiwwLHsib2Zmc2V0IjotMn1dLFsyLDMsIiIsMCx7Im9mZnNldCI6Mn1dLFszLDQsIiIsMCx7Im9mZnNldCI6LTJ9XSxbMyw0LCIiLDAseyJvZmZzZXQiOjJ9XSxbNCw1XSxbMyw2XSxbNiw3LCIiLDAseyJvZmZzZXQiOi0yfV0sWzcsOF0sWzUsOF0sWzEsNSwiIiwwLHsib2Zmc2V0IjotMn1dLFswLDQsIiIsMCx7Im9mZnNldCI6LTJ9XSxbNCw3XSxbMCw0LCIiLDAseyJvZmZzZXQiOjJ9XSxbMSw1LCIiLDAseyJvZmZzZXQiOjJ9XSxbNiw3LCIiLDAseyJvZmZzZXQiOjJ9XV0=
\[\begin{tikzcd}
	{A_1 \times A_2} & {B_1 \times A_2} & {C_1 \times A_2} \\
	{A_1 \times B_2} & {B_1 \times B_2} & {C_1 \times B_2} \\
	{A_1 \times C_2} & {B_1 \times C_2} & {C_1 \times C_2}
	\arrow[from=1-2, to=1-3]
	\arrow[shift left=2, from=1-1, to=1-2]
	\arrow[shift right=2, from=1-1, to=1-2]
	\arrow[shift left=2, from=1-1, to=2-1]
	\arrow[shift right=2, from=1-1, to=2-1]
	\arrow[shift left=2, from=2-1, to=2-2]
	\arrow[shift right=2, from=2-1, to=2-2]
	\arrow[from=2-2, to=2-3]
	\arrow[from=2-1, to=3-1]
	\arrow[shift left=2, from=3-1, to=3-2]
	\arrow[from=3-2, to=3-3]
	\arrow[from=2-3, to=3-3]
	\arrow[shift left=2, from=1-3, to=2-3]
	\arrow[shift left=2, from=1-2, to=2-2]
	\arrow[from=2-2, to=3-2]
	\arrow[shift right=2, from=1-2, to=2-2]
	\arrow[shift right=2, from=1-3, to=2-3]
	\arrow[shift right=2, from=3-1, to=3-2]
\end{tikzcd}\]
        All rows and columns are coequalisers, since functors of the form \( (-) \times D \) preserve coequalisers.
        It then follows that the lower right square is a pushout.
        By reflexivity, if \( k : B_1 \times B_2 \to D \) coequalises
        \[ f_1 \times f_2, g_1 \times g_2 : A_1 \times A_2 \rightrightarrows B_1 \times B_2 \]
        then it also coequalises \( B_1 \times A_2 \rightrightarrows B_1 \times B_2 \) and \( A_1 \times B_2 \rightrightarrows B_1 \times B_2 \), as they both factor through the diagonal pair.
        Therefore, it factors through the top and left edges of the lower right square, and hence through its diagonal.
    \end{enumerate}
\end{remark}
\begin{example}
    \begin{enumerate}
        \item The forgetful functor \( U : \mathbf{Gp} \to \mathbf{Set} \) satisfies the hypotheses of the crude monadicity theorem.
        Indeed, it has a left adjoint and reflects isomorphisms, and it creates reflexive coequalisers.
        Given a reflexive pair \( f, g : A \rightrightarrows B \) in \( \mathbf{Gp} \), consider its coequaliser \( h : UB \to C \) in \( \mathbf{Set} \).
        As reflexive coequalisers commute with products in \( \mathbf{Set} \),
        % https://q.uiver.app/#q=WzAsMyxbMCwwLCJVQSBcXHRpbWVzIFVBIl0sWzEsMCwiVUIgXFx0aW1lcyBVQiJdLFsyLDAsIkMgXFx0aW1lcyBDIl0sWzAsMSwiZiIsMCx7Im9mZnNldCI6LTJ9XSxbMSwyXSxbMCwxLCJnIiwyLHsib2Zmc2V0IjoyfV1d
\[\begin{tikzcd}
	{UA \times UA} & {UB \times UB} & {C \times C}
	\arrow["f", shift left=2, from=1-1, to=1-2]
	\arrow[from=1-2, to=1-3]
	\arrow["g"', shift right=2, from=1-1, to=1-2]
\end{tikzcd}\]
        is a coequaliser.
        So we obtain a binary operation \( C \times C \to C \) making \( h \) into a homomorphism, \( C \) into a group, and \( h \) a coequaliser in \( \mathbf{Gp} \).
        The same procedure applies for many other algebraic structures, such as rings, modules over a given ring, and lattices.
        For infinitary algebraic categories such as complete semilattices and complete lattices, we can use the precise monadicity theorem whenever a left adjoint exists.
        \item Any reflection is monadic.
        If \( I : \mathcal D \to \mathcal C \) is the inclusion of a reflective subcategory and \( f, g : A \rightrightarrows B \) is an \( I \)-split pair in \( \mathcal D \), then the splitting \( t : B \to A \) belongs to \( \mathcal D \), and so its composite \( ft = sh \) also lies in \( \mathcal D \).
        But \( \mathcal D \) is closed under limits that exist in \( \mathcal C \), so in particular it is closed under splittings of idempotents.
        \item Consider the composite adjunction
        % https://q.uiver.app/#q=WzAsMyxbMCwwLCJcXG1hdGhiZntTZXR9Il0sWzEsMCwiXFxtYXRoYmZ7QWJHcH0iXSxbMiwwLCJcXG1hdGhiZnt0ZkFiR3B9Il0sWzAsMSwiRiIsMCx7Im9mZnNldCI6LTJ9XSxbMSwyLCJMIiwwLHsib2Zmc2V0IjotMn1dLFsxLDAsIlUiLDAseyJvZmZzZXQiOi0yfV0sWzIsMSwiSSIsMCx7Im9mZnNldCI6LTJ9XV0=
\[\begin{tikzcd}
	{\mathbf{Set}} & {\mathbf{AbGp}} & {\mathbf{tfAbGp}}
	\arrow["F", shift left=2, from=1-1, to=1-2]
	\arrow["L", shift left=2, from=1-2, to=1-3]
	\arrow["U", shift left=2, from=1-2, to=1-1]
	\arrow["I", shift left=2, from=1-3, to=1-2]
\end{tikzcd}\]
        Both factors are monadic: we have already shown that \( F \dashv U \) is monadic, and \( L \dashv I \) is a reflection.
        However, the composite \( LF \dashv UI \) is not monadic.
        Indeed, free abelian groups are torsion-free, so the monad induced by the composite adjunction coincides with that induced by \( F \dashv U \).
        \item The contravariant power-set functor \( P^\star : \mathbf{Set}^\cop \to \mathbf{Set} \) is monadic as it satisfies the hypotheses of the crude monadicity theorem.
        Its left adjoint is \( P^\star : \mathbf{Set} \to \mathbf{Set}^\cop \), and it reflects isomorphisms.
        Let
        % https://q.uiver.app/#q=WzAsMyxbMCwwLCJBIl0sWzEsMCwiQiJdLFsyLDAsIkMiXSxbMCwxLCJlIl0sWzEsMiwiZiIsMCx7Im9mZnNldCI6LTJ9XSxbMSwyLCJnIiwyLHsib2Zmc2V0IjoyfV1d
\[\begin{tikzcd}
	A & B & C
	\arrow["e", from=1-1, to=1-2]
	\arrow["f", shift left=2, from=1-2, to=1-3]
	\arrow["g"', shift right=2, from=1-2, to=1-3]
\end{tikzcd}\]
        be a coreflexive equaliser in \( \mathbf{Set} \).
        Then the square
        % https://q.uiver.app/#q=WzAsNCxbMCwwLCJBIl0sWzEsMCwiQiJdLFsxLDEsIkMiXSxbMCwxLCJCIl0sWzAsMSwiZSJdLFsxLDIsImciXSxbMCwzLCJlIiwyXSxbMywyLCJmIiwyXV0=
\[\begin{tikzcd}
	A & B \\
	B & C
	\arrow["e", from=1-1, to=1-2]
	\arrow["g", from=1-2, to=2-2]
	\arrow["e"', from=1-1, to=2-1]
	\arrow["f"', from=2-1, to=2-2]
\end{tikzcd}\]
        is a pullback.
        Thus, the composite
        % https://q.uiver.app/#q=WzAsMyxbMCwwLCJQQiJdLFsxLDAsIlBBIl0sWzIsMCwiUEIiXSxbMCwxLCJQXlxcc3RhciBlIl0sWzEsMiwiUGUiXV0=
\[\begin{tikzcd}
	PB & PA & PB
	\arrow["{P^\star e}", from=1-1, to=1-2]
	\arrow["Pe", from=1-2, to=1-3]
\end{tikzcd}\]
        coincides with
        % https://q.uiver.app/#q=WzAsMyxbMCwwLCJQQiJdLFsxLDAsIlBDIl0sWzIsMCwiUEIiXSxbMCwxLCJQZyJdLFsxLDIsIlBeXFxzdGFyIGYiXV0=
\[\begin{tikzcd}
	PB & PC & PB
	\arrow["Pg", from=1-1, to=1-2]
	\arrow["{P^\star f}", from=1-2, to=1-3]
\end{tikzcd}\]
        Also, \( (P^\star e)(Pe) = 1_{PA} \) and \( (P^\star g)(Pg) = 1_{PB} \), so we obtain the following split coequaliser diagram in \( \mathbf{Set} \).
        % https://q.uiver.app/#q=WzAsMyxbMCwwLCJQQyJdLFsxLDAsIlBCIl0sWzIsMCwiUEEiXSxbMCwxLCJQXlxcc3RhciBmIiwwLHsib2Zmc2V0IjotNH1dLFsxLDIsIlBeXFxzdGFyIGUiLDAseyJvZmZzZXQiOi0yfV0sWzAsMSwiUF5cXHN0YXIgZyIsMl0sWzEsMCwiUGciLDAseyJvZmZzZXQiOi0yLCJjdXJ2ZSI6LTJ9XSxbMiwxLCJQZSIsMCx7ImN1cnZlIjotMn1dXQ==
\[\begin{tikzcd}[column sep=large]
	PC & PB & PA
	\arrow["{P^\star f}", shift left=4, from=1-1, to=1-2]
	\arrow["{P^\star e}", shift left=2, from=1-2, to=1-3]
	\arrow["{P^\star g}"', from=1-1, to=1-2]
	\arrow["Pg", shift left=2, curve={height=-12pt}, from=1-2, to=1-1]
	\arrow["Pe", curve={height=-12pt}, from=1-3, to=1-2]
\end{tikzcd}\]
        \item The forgetful functor \( U : \mathbf{Top} \to \mathbf{Set} \) is not monadic.
        The monad induced by \( D \dashv U \) is \( 1_{\mathbf{Set}} \), and the unit and multiplication are the identity natural transformations.
        Hence its category of algebras is isomorphic to \( \mathbf{Set} \).
        This example demonstrates that reflection of isomorphisms is necessary for the crude theorem.
        \item The composite
        % https://q.uiver.app/#q=WzAsMyxbMCwwLCJcXG1hdGhiZntTZXR9Il0sWzEsMCwiXFxtYXRoYmZ7VG9wfSJdLFsyLDAsIlxcbWF0aGJme0tIYXVzfSJdLFswLDEsIkQiLDAseyJvZmZzZXQiOi0yfV0sWzEsMiwiXFxiZXRhIiwwLHsib2Zmc2V0IjotMn1dLFsxLDAsIlUiLDAseyJvZmZzZXQiOi0yfV0sWzIsMSwiSSIsMCx7Im9mZnNldCI6LTJ9XV0=
\[\begin{tikzcd}
	{\mathbf{Set}} & {\mathbf{Top}} & {\mathbf{KHaus}}
	\arrow["D", shift left=2, from=1-1, to=1-2]
	\arrow["\beta", shift left=2, from=1-2, to=1-3]
	\arrow["U", shift left=2, from=1-2, to=1-1]
	\arrow["I", shift left=2, from=1-3, to=1-2]
\end{tikzcd}\]
        is monadic, where \( \beta \) is the Stone--\v{C}ech compactification functor; we will prove this using the precise monadicity theorem.
        Consider a \( UI \)-split pair \( f, g : X \rightrightarrows Y \) in \( \mathbf{KHaus} \).
        % https://q.uiver.app/#q=WzAsMyxbMCwwLCJVWCJdLFsxLDAsIlVZIl0sWzIsMCwiWiJdLFswLDEsIlVmIiwwLHsib2Zmc2V0IjotNH1dLFsxLDIsImgiLDAseyJvZmZzZXQiOi0yfV0sWzAsMSwiVWciLDJdLFsxLDAsInQiLDAseyJvZmZzZXQiOi0yLCJjdXJ2ZSI6LTJ9XSxbMiwxLCJzIiwwLHsiY3VydmUiOi0yfV1d
\[\begin{tikzcd}[column sep=large]
	UX & UY & Z
	\arrow["Uf", shift left=4, from=1-1, to=1-2]
	\arrow["h", shift left=2, from=1-2, to=1-3]
	\arrow["Ug"', from=1-1, to=1-2]
	\arrow["t", shift left=2, curve={height=-12pt}, from=1-2, to=1-1]
	\arrow["s", curve={height=-12pt}, from=1-3, to=1-2]
\end{tikzcd}\]
        There is a unique topology on \( Z \) making \( h \) into a coequaliser in \( \mathbf{Top} \), which is the quotient topology.
        This is compact as it is a continuous image of the compact space \( Y \).
        Hence \( h \) will be a coequaliser in \( \mathbf{KHaus} \) if and only if this topology is Hausdorff.
        Note that the quotient topology is the only possible candidate topology on \( Z \) that could make \( h \) into a morphism in \( \mathbf{KHaus} \).

        It is a general fact that for every compact Hausdorff space \( Y \) and equivalence relation \( S \subseteq Y \times Y \), the quotient is Hausdorff if and only if \( S \) is closed as a subset of \( Y \times Y \).
        Suppose \( (y_1, y_2) \in S \), so \( h(y_1) = h(y_2) \).
        Then the elements \( x_1 = t(y_1) \) and \( x_2 = t(y_2) \) satisfy
        \[ g(x_1) = y_1;\quad g(x_2) = y_2;\quad f(x_1) = f(x_2) \]
        and if \( x_1, x_2 \) satisfy these three equations, then \( h(y_1) = h(y_2) \).
        Thus \( S \) is the image under \( g \times g : X \times X \to Y \times Y \) of the equivalence relation \( R \) on \( X \) given by \( \qty{(x_1, x_2) \mid f(x_1) = f(x_2)} \).
        But \( R \) is closed in \( X \times X \), as it is the equaliser of \( f \pi_1, f \pi_2 : X \times X \rightrightarrows Y \) into a Hausdorff space, so it is compact.
        Hence \( S \) is compact, and thus closed.
    \end{enumerate}
\end{example}
\begin{definition}
    Let \( F \dashv G \) be an adjunction with \( F : \mathcal C \to \mathcal D, G : \mathcal D \to \mathcal C \).
    Suppose that \( \mathcal D \) has reflexive coequalisers.
    The \emph{monadic tower} of \( F \dashv G \) is the diagram
    % https://q.uiver.app/#q=WzAsNSxbMiw1LCJcXG1hdGhjYWwgQyJdLFswLDMsIlxcbWF0aGNhbCBEIl0sWzIsMywiXFxtYXRoY2FsIENee1xcbWF0aGJiIFR9Il0sWzIsMSwiKFxcbWF0aGNhbCBDXntcXG1hdGhiYiBUfSlee1xcbWF0aGJiIFN9Il0sWzIsMF0sWzAsMSwiRiIsMCx7Im9mZnNldCI6LTIsImN1cnZlIjotMn1dLFsxLDAsIkciLDAseyJvZmZzZXQiOi0yLCJjdXJ2ZSI6Mn1dLFswLDIsIiIsMCx7Im9mZnNldCI6LTJ9XSxbMiwwLCIiLDAseyJvZmZzZXQiOi0yfV0sWzMsMiwiIiwyLHsib2Zmc2V0IjotMn1dLFsyLDMsIiIsMix7Im9mZnNldCI6LTJ9XSxbMiwxLCJMIiwyLHsib2Zmc2V0IjoyLCJzaG9ydGVuIjp7InRhcmdldCI6MTB9fV0sWzEsMiwiSyIsMix7Im9mZnNldCI6Miwic2hvcnRlbiI6eyJzb3VyY2UiOjEwfX1dLFsxLDMsIiIsMix7Im9mZnNldCI6MiwiY3VydmUiOi0yfV0sWzMsMSwiIiwyLHsib2Zmc2V0IjoyLCJjdXJ2ZSI6Mn1dLFszLDQsIlxcY2RvdHMiLDMseyJzdHlsZSI6eyJib2R5Ijp7Im5hbWUiOiJub25lIn0sImhlYWQiOnsibmFtZSI6Im5vbmUifX19XV0=
\[\begin{tikzcd}
	&& {} \\
	&& {(\mathcal C^{\mathbb T})^{\mathbb S}} \\
	\\
	{\mathcal D} && {\mathcal C^{\mathbb T}} \\
	\\
	&& {\mathcal C}
	\arrow["F", shift left=2, curve={height=-12pt}, from=6-3, to=4-1]
	\arrow["G", shift left=2, curve={height=12pt}, from=4-1, to=6-3]
	\arrow[shift left=2, from=6-3, to=4-3]
	\arrow[shift left=2, from=4-3, to=6-3]
	\arrow[shift left=2, from=2-3, to=4-3]
	\arrow[shift left=2, from=4-3, to=2-3]
	\arrow["L"', shift right=2, shorten >=5pt, from=4-3, to=4-1]
	\arrow["K"', shift right=2, shorten <=5pt, from=4-1, to=4-3]
	\arrow[shift right=2, curve={height=-12pt}, from=4-1, to=2-3]
	\arrow[shift right=2, curve={height=12pt}, from=2-3, to=4-1]
	\arrow["\cdots"{marking, allow upside down}, draw=none, from=2-3, to=1-3]
\end{tikzcd}\]
    where \( \mathbb T \) is the monad induced by \( F \dashv G \), \( K \) is the comparison functor, \( L \) is the left adjoint to \( K \) which exists as \( \mathcal D \) has reflexive coequalisers, \( \mathbb S \) is the monad induced by \( L \dashv K \), and so on.
    We say that \( F \dashv G \) has \emph{monadic length} \( n \), or that \( \mathcal D \) has \emph{monadic height} \( n \) over \( \mathcal C \), if the tower reaches an equivalence after \( n \) steps.
\end{definition}
If \( F \dashv G \) is an equivalence, it has monadic length zero.
Monadic length one means that \( F \dashv G \) is monadic but not an equivalence, and example (iii) above has monadic length two.
% TODO: which example?
